Nuprl Definition : es-real 0,22
es.P(es) == R:Realizer. R ||- es.P(es) 
latex

clarification:

es-real{i:l}(es.P(es)) == R:es_realizer{i:l}. R ||-{i} es.P(es) 
latex

Definitionsx:A. B(x), Realizer, R ||- es.P(es)
FDL editor aliaseses-real

origin